Nuprl Lemma : msg_wf
11,40
postcript
pdf
M
:(IdLnk
Id
Type),
l
:IdLnk,
t
:Id,
v
:
M
(
l
,
t
). msg(
l
;
t
;
v
)
Msg(
M
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Msg(
M
)
,
msg(
l
;
t
;
v
)
Lemmas
Id
wf
,
IdLnk
wf
origin
M:(IdLnk
IdType), l:IdLnk, t:Id, v:M(l,t). msg(l; t; v) 
Msg(M) M:(IdLnkIdType), l:IdLnk, t:Id, v:M(l,t). msg(l; t; v) Msg(M) x:A. B(x) T